Skip to content

Conversation

phansch
Copy link
Contributor

@phansch phansch commented Oct 13, 2019

report_time was renamed to time_options and is now an Option.

First step of fixing Clippy and Miri toolstate after rust-lang/rust#64873

`report_time` was renamed to `time_options` and is now an `Option`.
@phansch
Copy link
Contributor Author

phansch commented Oct 13, 2019

The PR fails because rust-lang/rust#64873 is not in a nightly yet. Since CI here is using nightly rust, we would have to wait until the next nightly for a green build.

@phansch
Copy link
Contributor Author

phansch commented Oct 13, 2019

Oh also #187 and #188 would have to be merged for a completely green build.

@phansch
Copy link
Contributor Author

phansch commented Oct 13, 2019

Fixing the merge conflict, one sec 😅

@Manishearth Manishearth merged commit 71c2743 into Manishearth:master Oct 13, 2019
@phansch
Copy link
Contributor Author

phansch commented Oct 13, 2019

oh, you did it, thanks! =)

@phansch phansch deleted the fix_build branch October 13, 2019 14:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants